signature PTRPROOF_STRUCTS =
sig
  structure Irvc2vc : IRVC2VC
end

signature PTRPROOF =
sig
  include PTRPROOF_STRUCTS
  
  val top : Irvc2vc.Ir.Program.t -> unit
end
